package probsym.concurrent;

//import gov.nasa.jpf.symbc.probsym.Analyze;

/* 
 * Script to run for f in `seq 200`; do java probsym.concurrent.SmallConcurrentTest;done > results 
 */

import java.util.concurrent.BrokenBarrierException;
import java.util.concurrent.CyclicBarrier;

public class SmallConcurrentTest {

	static final CyclicBarrier gate = new CyclicBarrier(3);
	static int result = 0;
	
	public void startit() throws InterruptedException, BrokenBarrierException {
		SharedData sd = new SharedData();
		T1 t1 = new T1(sd);
		T2 t2 = new T2(sd);
		t2.start();
		t1.start();
		gate.await();
	}
	
	public static void main(String[] args) throws InterruptedException, BrokenBarrierException {
		SmallConcurrentTest sct = new SmallConcurrentTest();
		sct.startit();
	}
	
	public int getResult() {
		return result;
	}

}

class SharedData {
	int x = 0;
}
class T1 extends Thread {
	
	SharedData sd;
	public T1(SharedData s) {
		this.sd = s;
	}
	
	public void run() {
		try {
			SmallConcurrentTest.gate.await();
		} catch (InterruptedException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		} catch (BrokenBarrierException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		}
		sd.x++;
	}
}

class T2 extends Thread {
	
	SharedData sd;
	public T2(SharedData s) {
		this.sd = s;
	}	
	
	public void run() {
		try {
			SmallConcurrentTest.gate.await();
		} catch (InterruptedException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		} catch (BrokenBarrierException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		}
		sd.x++;
		int tmp = sd.x;
		SmallConcurrentTest.result = tmp;
		System.out.println(tmp);
		/*
		if (tmp == 0) {
			Analyze.coverage(""+0);
		} else if (tmp == 1){
			Analyze.coverage(""+1);
			System.out.println("1");			
		} else if (tmp == 2) {
			Analyze.coverage(""+2);
			System.out.println("2");
		} else {
			Analyze.coverage(""+3);
		}
		*/
	}
}

